Abstract: Bell-La Padula (BLP) model is a classical data confidentiality model and is often used as a security policy model in the researches of high-grade secure operating systems. But as its own shortages, it is hard to satisfy the requirement of development in actual systems. By doing the corresponding improvement and formal description, it can be used in actual systems and also satisfies the requirement of formal security policy model in the development of access verification and protection level of secure operating systems according to the “Information security technology: Security techniques requirement for operating system” (GB/T 20272-2006).

Key words: BLP model, security policy, formal method, secure transition rule, secure operating system